Nuprl Lemma : assoced_functionality_wrt_assoced
2,24
postcript
pdf
a
,
b
,
a'
,
b'
:
. (
a
~
a'
)
(
b
~
b'
)
((
a
~
b
)
(
a'
~
b'
))
latex
Definitions
x
,
y
.
t
(
x
;
y
)
,
P
Q
,
{
T
}
,
a
~
b
,
x
:
A
.
B
(
x
)
,
t
T
Lemmas
assoced
equiv
rel
,
assoced
wf
,
equiv
rel
self
functionality
origin
a, b, a', b':
. (a ~ a') 
(b ~ b') ((a ~ b) 
(a' ~ b')) a, b, a', b':. (a ~ a') (b ~ b') ((a ~ b) (a' ~ b')) 
x,y. t(x;y) Qx:A. B(x)
T